/**
 * Copyright (c) 2010 CWI Amsterdam and others. All rights reserved.
 * This program and the accompanying materials are made available
 * under the terms of the Eclipse Public License v1.0
 * which accompanies this distribution, and is available at
 * http://www.eclipse.org/legal/epl-v10.html
 * 
 * Contributors:
 *    CWI Amsterdam - initial API and implementation
 */
package nl.cwi.arne.mcrl2.toolchains;

import java.io.File;

import nl.cwi.arne.mcrl2.Specification;
import nl.cwi.arne.mcrl2.util.Command;
import nl.cwi.arne.mcrl2.util.MCRL2Commands;
import nl.cwi.arne.mcrl2.util.MCRL2FileUtil;
import nl.cwi.arne.mcrl2.util.MCRL2Options;

/**
 * @author Christian Krause
 * @generated NOT
 */
public final class VerifyFormulaToolChain extends GenerateLPSToolChain {

	// Default serial ID:
	private static final long serialVersionUID = 1L;
	
	// Involved files:
	private File mcfFile, pbesFile;
	
	// pbes2bool command:
	private Command pbes2boolCommand;
	
	// Whether we should delete the mcf file afterwards:
	private boolean deleteMcfFile = true;
	
	// Result:
	private boolean result;
	
	/**
	 * Constructor.
	 * @param specification mCRL2 Specification.
	 * @param options Options
	 */
	public VerifyFormulaToolChain(Specification specification, String formula, MCRL2Options options) {
		super(specification, options);		
		this.mcfFile = MCRL2FileUtil.saveFormula(formula);
		initToolChain(options);
	}

	/**
	 * Alternative constructor.
	 * @param lpsFile LPS file.
	 * @param formula Model formula.
	 * @param options Options.
	 */
	public VerifyFormulaToolChain(File lpsFile, String formula, MCRL2Options options) {
		super(lpsFile);
		this.mcfFile = MCRL2FileUtil.saveFormula(formula);
		initToolChain(options);
	}
	
	/**
	 * Alternative constructor.
	 * @param lpsFile LPS file.
	 * @param mcfFile MCF File.
	 * @param options Options.
	 */
	public VerifyFormulaToolChain(File lpsFile, File mcfFile, MCRL2Options options) {
		super(lpsFile);
		setCaptureOutput(true);
		this.mcfFile = mcfFile;
		initToolChain(options);
	}
	
	/*
	 * (non-Javadoc)
	 * @see nl.cwi.arne.mcrl2.util.ToolChain#setCaptureOutput(boolean)
	 */
	@Override
	public void setCaptureOutput(boolean print) {
		if (!print) {
			throw new IllegalArgumentException("VerifyFormulaToolChain needs to capture the output to compute the result");
		}
		super.setCaptureOutput(true);
	}
	
	/*
	 * Initialize this tool chain.
	 */
	private void initToolChain(MCRL2Options options) {
		
		setName("Verifying model formula...");
		setWaitForLast(true);
		
		pbesFile = new File(getBaseFileName() + ".pbes");
		add(MCRL2Commands.lps2pbes(getLPSFile(), mcfFile, pbesFile));
		add(pbes2boolCommand = MCRL2Commands.pbes2bool(pbesFile));

	}
	
	/*
	 * (non-Javadoc)
	 * @see nl.cwi.arne.mcrl2.util.ToolChain#commandFinished(nl.cwi.arne.mcrl2.util.ToolChain.Command)
	 */
	@Override
	protected void commandFinished(Command command) {
		super.commandFinished(command);
		
		// Parse output of pbes2bool:
		if (command==pbes2boolCommand) {
			String output = pbes2boolCommand.getOutput().trim();
			if (output.endsWith("true")) {
				result = true;
			} else if (output.endsWith("false")) {
				result = false;
			} else {
				pbes2boolCommand.setExitCode(UNEXPECTED_OUTPUT_EXIT_CODE);
			}
		}

	}
	
	/*
	 * (non-Javadoc)
	 * @see nl.cwi.arne.mcrl2.toolchains.GenerateLPSToolChain#doCleanup()
	 */
	@Override
	protected void doCleanup() {
		super.doCleanup();
		pbesFile.delete();
		if (deleteMcfFile) {
			mcfFile.delete();
		}
	}
	
	public boolean getResult() {
		return result;
	}
	
	public void setDeleteMCFFile(boolean delete) {
		this.deleteMcfFile = delete;
	}
}